Termination Proof Script
Consider the TRS R consisting of the rewrite rules
|
| 1: |
|
fac(0) |
→ 1 |
| 2: |
|
fac(s(x)) |
→ s(x) * fac(x) |
| 3: |
|
floop(0,y) |
→ y |
| 4: |
|
floop(s(x),y) |
→ floop(x,s(x) * y) |
| 5: |
|
x * 0 |
→ 0 |
| 6: |
|
x * s(y) |
→ (x * y) + x |
| 7: |
|
x + 0 |
→ x |
| 8: |
|
x + s(y) |
→ s(x + y) |
| 9: |
|
1 |
→ s(0) |
| 10: |
|
fac(0) |
→ s(0) |
|
There are 8 dependency pairs:
|
| 11: |
|
FAC(0) |
→ 1# |
| 12: |
|
FAC(s(x)) |
→ s(x) *# fac(x) |
| 13: |
|
FAC(s(x)) |
→ FAC(x) |
| 14: |
|
FLOOP(s(x),y) |
→ FLOOP(x,s(x) * y) |
| 15: |
|
FLOOP(s(x),y) |
→ s(x) *# y |
| 16: |
|
x *# s(y) |
→ (x * y) +# x |
| 17: |
|
x *# s(y) |
→ x *# y |
| 18: |
|
x +# s(y) |
→ x +# y |
|
The approximated dependency graph contains 4 SCCs:
{18},
{17},
{14}
and {13}.
-
Consider the SCC {18}.
There are no usable rules.
By taking the AF π with
π(+#) = 2 together with
the lexicographic path order with
empty precedence,
rule 18
is strictly decreasing.
-
Consider the SCC {17}.
There are no usable rules.
By taking the AF π with
π(*#) = 2 together with
the lexicographic path order with
empty precedence,
rule 17
is strictly decreasing.
-
Consider the SCC {14}.
The usable rules are {5-8}.
By taking the AF π with
π(FLOOP) = 1 together with
the lexicographic path order with
precedence * ≻ + ≻ s,
the rules in {5-8,14}
are strictly decreasing.
-
Consider the SCC {13}.
There are no usable rules.
By taking the AF π with
π(FAC) = 1 together with
the lexicographic path order with
empty precedence,
rule 13
is strictly decreasing.
Hence the TRS is terminating.
Tyrolean Termination Tool (0.02 seconds)
--- May 3, 2006